Iof proof for Lemma append overlapping sublists:
1. T : Type
2. L1 : T List
3. L2 : T List
4. L : T List
5. x : T
6.
i, j:
. (i < ||L||) 
(j < ||L||) (
(i = j)) ((L[i] = L[j]))
7. f1 : {0..||L1 @ [x]||
}
{0..||L||}
8. increasing(f1;||L1 @ [x]||)
9.
j:{0..||L1 @ [x]||}. (L1 @ [x])[j] = L[(f1(j))]
10. f : {0..(||L2||+1)
}{0..||L||}
11. increasing(f;||L2||+1)
12.
j:{0..(||L2||+1)}. [x / L2][j] = L[(f(j))]
13. ||L1 @ [x / L2]|| = ||L1||+||L2||+1
14. ||[]||
0
increasing(
i.if i 
z ||L1|| then f1(i) else f(i - ||L1||) fi ;||L1 @ [x / L2]||)
& (j:{0..||L1 @ [x / L2]||}.
& ((L1 @ [x / L2])[j] = L[((i.if i z ||L1|| then f1(i) else f(i - ||L1||) fi )(j))])
by ((Reduce 0)
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok SupInf:t) inil_term)))
C1:
C1: increasing(i.if i z ||L1|| then f1(i) else f(i - ||L1||) fi ;||L1 @ [x / L2]||)
C2:
C2: 15. j : {0..||L1 @ [x / L2]||}
C2: (L1 @ [x / L2])[j] = L[if j z ||L1|| then f1(j) else f(j - ||L1||) fi ]
C.
T